es:ES, P:(E), j:E. (e:E. (e < j)  Dec(P(e)))  Dec(k:E. ((k < j) & P(k))) 

latex

Definitions	P  Q, P  Q, {T}, A, A c B, P  Q, Dec(P), P & Q, x:A. B(x), x(s), x:A. B(x), P  Q, t  T, , False
Lemmas	es-pred-causl, and functionality wrt iff, es-sender wf, es-pred wf, assert wf, es-causl-iff, not wf, es-sender-causl, es-isrcv wf, es-first wf, decidable assert, event system wf, es-causle weakening, es-causl transitivity2, decidable wf, es-causl wf, es-E wf